theory SemReach2 imports Main ClangSem ClangEv
begin

fun isnone where "isnone (Cnone _) = True" | "isnone _ = False"

fun anoncl :: "(('pn,'m,'n,'l) stmt \<Rightarrow> bool) \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
where
  "anoncl A (Cnone lb) = A (Cnone lb)"
| "anoncl A (Cseq lb s1 s2) = ((isnone s1 \<or> anoncl A s1) \<and> A s2 \<and> anoncl A s2)"
| "anoncl A (Casg lb x e) = A (Cnone lb)"
| "anoncl A (Cif lb be s1 s2) = ((A s1 \<and> anoncl A s1) \<or> (A s2 \<and> anoncl A s2))"
| "anoncl A (Cread lb x y) = A (Cnone lb)"
| "anoncl A (Cwrite lb x y) = A (Cnone lb)"
| "anoncl A (Cwhile lb be s) = A (Cnone lb)"
| "anoncl A (Cwait lb wcs s) = anoncl A s"

definition anoncls :: "(('pn,'m,'n,'l) stmt \<Rightarrow> bool) \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
where
  "anoncls A s = (isnone s \<or> anoncl A s)"

(* note: does not track Cseq labels *)
fun aclwh:: "(('pn,'m,'n,'l) stmt \<Rightarrow> bool) \<Rightarrow> 'l option \<Rightarrow> 'm bexpr \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool" 
and aclseq :: "(('pn,'m,'n,'l) stmt \<Rightarrow> bool) \<Rightarrow> 'l option \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
and astmcl :: "(('pn,'m,'n,'l) stmt \<Rightarrow> bool) \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> ('pn,'m,'n,'l) stmt \<Rightarrow> bool"
where
  "aclwh A lb be s (Cseq lb' s1' s2') = (A s \<and> astmcl A s s1' \<and> s2' = (Cwhile lb be s))"
| "aclwh A lb be s s' = (s' = (Cwhile lb be s) \<or> s' = (Cnone lb))"

| "aclseq A lb s1 s2 (Cseq lb' s1' s2') = (((astmcl A s1 s1') \<and> s2 = s2') \<or> (anoncls A s1 \<and> A s2 \<and> astmcl A s2 (Cseq lb' s1' s2')))"
| "aclseq A lb s1 s2 s' = (anoncls A s1 \<and> A s2 \<and> astmcl A s2 s')"

| "astmcl A (Cnone lb) s'        = (A s' \<and> s' = (Cnone lb))"
| "astmcl A (Cseq lb s1 s2) s'   = (A s' \<and> (s' = (Cseq lb s1 s2)   \<or> aclseq A lb s1 s2 s'))"
| "astmcl A (Casg lb x e) s'     = (A s' \<and> (s' = (Casg lb x e)     \<or> s' = (Cnone lb)))"
| "astmcl A (Cif lb be s1 s2) s' = (A s' \<and> (s' = (Cif lb be s1 s2) \<or> (A s1 \<and> astmcl A s1 s') \<or> (A s2 \<and> astmcl A s2 s')))"
| "astmcl A (Cwhile lb be s) s'  = (A s' \<and> (s' = (Cwhile lb be s)  \<or> aclwh A lb be s s'))"
| "astmcl A (Cread lb x y) s'    = (A s' \<and> (s' = (Cread lb x y)    \<or> s' = (Cnone lb)))"
| "astmcl A (Cwrite lb x y) s'   = (A s' \<and> (s' = (Cwrite lb x y)   \<or> s' = (Cnone lb)))"
| "astmcl A (Cwait lb wcs s) s'  = (A s' \<and> (s' = (Cwait lb wcs s)  \<or> astmcl A s s'))"

definition "seqcond A = (\<forall> x y z . A (Cseq x y z) \<longrightarrow> A y)"

lemma astmcl_end: "astmcl A s1 s2 \<Longrightarrow> A s2" by (induct s1, auto)

lemma anoncl_expr: "anoncl A s = (\<exists> lb . astmcl A s (Cnone lb))"
apply(induct s, simp_all)
apply(metis anoncls_def astmcl_end)
apply(metis anoncls_def astmcl_end)
apply(metis anoncls_def astmcl_end)
done

lemma anoncls_expr: "anoncls A s = (isnone s \<or> (\<exists> lb . astmcl A s (Cnone lb)))"
  using anoncl_expr anoncls_def (*by (auto, cases s, simp_all)*) by (auto)

lemma astmcl_fix: "A s \<Longrightarrow> astmcl A s s" by (cases s, simp_all)
lemma aclseq_fix: "A s2 \<Longrightarrow> aclseq A lb (Cnone lb') s2 s2" by (cases s2, simp_all add: anoncls_expr)

lemma lem_aclseq_ex: "aclseq A lb s1 s2 s' = ((anoncls A s1 \<and> A s2 \<and> astmcl A s2 s') \<or> (\<exists> lb' s1' . astmcl A s1 s1' \<and> s' = (Cseq lb' s1' s2)))"
  by (cases s', auto)

lemma lem_astmcl_he1:
  assumes acond: "seqcond A"
  and a0: "s = (Cseq lb s1 s2)"
  and a1:"\<forall> s1' . A s1' \<and> transition s1 q io s1' q' \<longrightarrow> astmcl A s1 s1'"
  and a2: "A s'" "transition s q io s' q'"
  shows "astmcl A s s'"
using a0 a2
apply(cases s, simp_all)
apply(case_tac "\<exists> x . stmt1 = Cnone x", simp_all add: astmcl_fix) (*1 goal*)
apply(clarify)
apply(simp add: astmcl_fix)
apply(simp add: aclseq_fix)
proof - (* s' is Cseq *)
  fix lbx s1x s2x
  assume c0: "lbx = lb \<and> s1x = s1 \<and> s2x = s2"
  assume c1: "s = Cseq lb s1 s2" "A s'"
  assume c2:"case s1 of Cnone x \<Rightarrow> s' = s2 \<and> io = ANone \<and> q' = q | _ \<Rightarrow> (case s' of Cseq None s1' s2' \<Rightarrow> s2' = s2 \<and> transition s1 q io s1' q' | Cseq (Some a) s1' s2' \<Rightarrow> False | _ \<Rightarrow> False)" "\<forall>x. s1 \<noteq> Cnone x"
  then have "case s' of Cseq None s1' s2' \<Rightarrow> s2' = s2 \<and> transition s1 q io s1' q' | Cseq (Some a) s1' s2' \<Rightarrow> False | _ \<Rightarrow> False"
    by (cases s1, simp_all)
  from this c1 show "s' = (Cseq lb s1 s2) \<or> aclseq A lb s1 s2 s'"
    apply(cases s', simp_all)
    apply(case_tac "option", simp_all)
    proof -
      fix option stmt1 stmt2
      assume "stmt2 = s2 \<and> transition s1 q io stmt1 q'" "A (Cseq None stmt1 s2)" "s' = Cseq None stmt1 s2" "s = Cseq lb s1 s2" "option = None"
      moreover then have "astmcl A s1 stmt1" using a1 acond seqcond_def by metis
      ultimately show "None = lb \<and> stmt1 = s1 \<or> astmcl A s1 stmt1 \<or> (anoncls A s1 \<and> A s2 \<and> astmcl A s2 (Cseq None stmt1 s2))"
        by (cases s1, simp_all)
    qed
qed

lemma lem_astmcl_he2:
assumes acond: "seqcond A"
shows "\<forall> s' . A s' \<and> transition s q io s' q' \<longrightarrow> astmcl A s s'"
apply(induct s)
apply(simp)                      --"Cnone"
apply(metis acond lem_astmcl_he1) --"Cseq"
apply(case_tac "expr", simp_all) --"Casg, Cread, Cwrite"
apply(case_tac "eval_bexpr q bexpr", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: astmcl_fix)
apply(simp add: astmcl_fix)       --"Cif"
apply(case_tac "eval_bexpr q bexpr", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(clarify)
apply(case_tac "s'", simp_all)
apply(subgoal_tac "A s")
apply(simp add: astmcl_fix)
apply(metis acond seqcond_def)     --"Cwhile"
apply(simp add: astmcl_fix)       --"Cwait"
done

lemma lem_astmcl:
  assumes acond: "seqcond A"
  shows "A s' \<and> transition s q io s' q' \<Longrightarrow> astmcl A s s'" --"soundness"
using acond lem_astmcl_he2 by blast

lemma anoncls_aft_astmcl:
  assumes a1:"\<forall> s3 . A s3 \<and> astmcl A s1 s2 \<and> astmcl A s2 s3 \<longrightarrow> astmcl A s1 s3"
  shows "astmcl A s1 s2 \<Longrightarrow> anoncls A s2 \<Longrightarrow> anoncls A s1"
apply(auto simp only: anoncls_expr)
apply(cases s2, simp_all)
apply(case_tac "A (Cnone lb)")
apply(metis a1)
apply(subgoal_tac "anoncls A s2")
defer
apply(metis anoncls_expr)
apply(induct s2, simp_all)
done

lemma astmcl_trans_he:
  assumes acond: "seqcond A"
  shows "\<forall> s2 s3 . A s3 \<and> astmcl A s1 s2 \<and> astmcl A s2 s3 \<longrightarrow> astmcl A s1 s3"
apply(induct s1)
apply(auto)
proof -
  fix lb s11 s12 s2 s3
  assume a2:"A s3" "astmcl A s2 s3" "A s2" "aclseq A lb s11 s12 s2"
  assume a3: "\<not> aclseq A lb s11 s12 s3"
  assume a0:"\<forall>s2 s3. A s3 \<and> astmcl A s11 s2 \<and> astmcl A s2 s3 \<longrightarrow> astmcl A s11 s3"
  assume a1:"\<forall>s2 s3. A s3 \<and> astmcl A s12 s2 \<and> astmcl A s2 s3 \<longrightarrow> astmcl A s12 s3"
  have zz1:"(\<exists> lb' s1'. astmcl A s11 s1' \<and> s2 = Cseq lb' s1' s12) \<longrightarrow> aclseq A lb s11 s12 s3"
  proof
    assume "\<exists> lb' s1'. astmcl A s11 s1' \<and> s2 = Cseq lb' s1' s12"
    then obtain lb' s1' where c1:"astmcl A s11 s1' \<and> s2 = Cseq lb' s1' s12" by blast
    from this a2 have "s3 = s2 \<or> aclseq A lb' s1' s12 s3" by auto
    moreover {
      assume "s3 = s2"
      from this a2 have "aclseq A lb s11 s12 s3" by simp
    }
    moreover {
      assume "aclseq A lb' s1' s12 s3"
      then have "(anoncls A s1' \<and> A s12 \<and> astmcl A s12 s3 \<or> (\<exists> lbx s1x . astmcl A s1' s1x \<and> s3 = (Cseq lbx s1x s12)))" using lem_aclseq_ex by blast
      moreover {
        assume "\<exists> lbx s1x . astmcl A s1' s1x \<and> s3 = (Cseq lbx s1x s12)"
        then obtain lbx s1x where "astmcl A s1' s1x \<and> s3 = (Cseq lbx s1x s12)" by blast
        moreover from this c1 a0 have "astmcl A s11 s1x" using a2(1) acond seqcond_def by metis
        ultimately have "(\<exists> lbx s1x. astmcl A s11 s1x \<and> s3 = Cseq lbx s1x s12)" by blast
      }
      moreover from c1 have "anoncls A s1' \<longrightarrow> anoncls A s11" using anoncls_aft_astmcl a0 by blast
      ultimately have "aclseq A lb s11 s12 s3" using a2 a1 lem_aclseq_ex by blast
    }
    ultimately show "aclseq A lb s11 s12 s3" by blast
  qed
  moreover from a2(4) have "anoncls A s11 \<and> A s12 \<and> astmcl A s12 s2 \<or> (\<exists>lb' s1'. astmcl A s11 s1' \<and> s2 = Cseq lb' s1' s12)" using lem_aclseq_ex by metis
  ultimately have "anoncls A s11 \<and> A s12" using a3 by metis
  from zz1 this a1 a2 a3 show "s3 = Cseq lb s11 s12" using lem_aclseq_ex by metis
next
  fix lb be s1 s2 s3
  assume a2: "astmcl A s2 s3" "aclwh A lb be s1 s2" "A s2"
  assume a3:"\<not> aclwh A lb be s1 s3"
  assume a0:"\<forall> s2 s3. A s3 \<and> astmcl A s1 s2 \<and> astmcl A s2 s3 \<longrightarrow> astmcl A s1 s3"
  from a2 have "aclwh A lb be s1 s3"
    apply(cases s2, auto)
    apply(cases s3, auto)
    apply(subgoal_tac "A stmt1a")
    apply(insert a0, blast)
    apply(metis acond seqcond_def)
    done
  from this a3 show "s3 = Cwhile lb be s1" by blast
qed

lemma astmcl_trans:
  assumes acond: "seqcond A"
  shows "A s3 \<Longrightarrow> astmcl A s1 s2 \<Longrightarrow> astmcl A s2 s3 \<Longrightarrow> astmcl A s1 s3" --"transitivity"
  using acond astmcl_trans_he by blast

(*------------------------------------------------------------------------------------------------------------------------------------------------------*)

lemma lem_etrans_astmcl:
  assumes acond: "seqcond A"
  shows "A (es_stm es') \<Longrightarrow> etrans (Some es) (Some es') \<Longrightarrow> astmcl A (es_stm es) (es_stm es')"
apply(cases es, cases es', auto)
apply(case_tac "bool")
apply(auto simp add: astmcl_fix lem_astmcl acond)
done

lemma lem_exseq_astmcl_he0:
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr"
  and a1:"exseq tr p i = Some es" "exseq tr p (Suc i) = Some es'"
  shows "A (es_stm es') \<Longrightarrow> astmcl A (es_stm es) (es_stm es')"
using a0 a1 acond exseq_trans lem_etrans_astmcl by metis

lemma lem_exseq_astmcl_he:
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr"
  shows "\<forall> i es' . ((\<forall> k \<in> {i..j} . \<forall> es' . (exseq tr p k) = Some es' \<longrightarrow> A (es_stm es')) \<and> exseq tr p i = Some es \<and> i \<le> j \<and> exseq tr p j = Some es' \<longrightarrow> astmcl A (es_stm es) (es_stm es'))"
apply(induct j)
apply(clarify)
apply(metis astmcl_fix atLeast0AtMost atMost_iff eq_imp_le option.inject) (*apply(metis astmcl_fix option.inject) apply(metis acond a0 lem_exseq_astmcl_he1) --"case i=0"*)
proof (clarify)
  fix j i es'
  assume c0:"\<forall>i es'. (\<forall>k\<in>{i..j}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')) \<and> exseq tr p i = Some es \<and> i \<preceq> j \<and> exseq tr p j = Some es' \<longrightarrow> astmcl A (es_stm es) (es_stm es')" "\<forall>k\<in>{i..Suc j}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')"
  assume c1:"exseq tr p i = Some es" "i \<preceq> Suc j" "exseq tr p (Suc j) = Some es'"
  from c0(2) c1 have c2:"A (es_stm es')" by auto
  from c1 have "i \<le> j \<or> i = Suc j" by auto
  moreover {
    assume d0:"i \<le> j"
    from a0 c1(3) obtain es1 where d1:"exseq tr p j = Some es1" using exseq_pre3 by metis
    from c0(2) this d0 have d2:"A (es_stm es1)" by auto
    from a0 d1 c1(3) have d3:"astmcl A (es_stm es1) (es_stm es')" using lem_exseq_astmcl_he0 acond c2 by simp
    from c0(2) have "\<forall>k\<in>{i..j}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')" by auto
    moreover from c1(1) c0(1) this d0 d1 have d4:"astmcl A (es_stm es) (es_stm es1)" by blast
    from d3 d4 have "astmcl A (es_stm es) (es_stm es')" using astmcl_trans acond c2 by blast
  }
  moreover {
    assume d0:"i = Suc j"
    from this c1 have "es = es'" by simp
    then have "astmcl A (es_stm es) (es_stm es')" using c2 astmcl_fix by blast 
  }
  ultimately show "astmcl A (es_stm es) (es_stm es')" by blast
qed

lemma lem_exseq_astmcl_closed:
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr" "i \<le> j" "exseq tr p i = Some es" "exseq tr p j = Some es'"
  and a1: "\<forall> k \<in> {i..j} . \<forall> es'' . (exseq tr p k) = Some es'' \<longrightarrow> A (es_stm es'')"
  shows "astmcl A (es_stm es) (es_stm es')"
using acond a0 a1 lem_exseq_astmcl_he by metis

lemma lem_exseq_astmcl:
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr" "i \<le> j" "exseq tr p i = Some es" "exseq tr p j = Some es'"
  and a1: "\<forall> k \<in> {i<..j} . \<forall> es'' . (exseq tr p k) = Some es'' \<longrightarrow> A (es_stm es'')"
  and a2: "A (es_stm es')"
  shows "astmcl A (es_stm es) (es_stm es')"
proof -
  from a0 have "Suc i \<le> j \<or> i = j" by auto
  moreover {
    assume c0:"Suc i \<le> j"
    moreover from this a0 obtain es1 where c1:"exseq tr p (Suc i) = Some es1" using etrans_cont exseq_trans by (metis not_Some_eq option.simps(3))
    moreover from a1 have "\<forall> k \<in> {Suc i..j} . \<forall> es'' . (exseq tr p k) = Some es'' \<longrightarrow> A (es_stm es'')" by auto
    ultimately have d1:"astmcl A (es_stm es1) (es_stm es')" using a0 acond lem_exseq_astmcl_closed by simp
    from a1 c1 c0 have "A (es_stm es1)" by auto
    from a0 c1 this have d2:"astmcl A (es_stm es) (es_stm es1)" using lem_exseq_astmcl_he0 acond by simp
    from d1 d2 have ?thesis using acond astmcl_end astmcl_trans by blast
  }
  moreover {
    assume "i = j"
    from this a0 a2 have ?thesis using astmcl_fix by simp 
  }
  ultimately show ?thesis by blast
qed

lemma lem_ntran_helper1: "\<forall> z . x \<le> z \<and> z \<le> (x+y) \<longrightarrow> f (z::nat) = f (Suc z) \<Longrightarrow> f x = f (Suc (x+y))" by (induct y, auto)
lemma lem_ntran_helper2: "x \<le> y \<Longrightarrow> \<forall> z . x \<le> z \<and> z \<le> y \<longrightarrow> f (z::nat) = f (Suc z) \<Longrightarrow> f x = f (Suc y)"
  using lem_ntran_helper1 [of x "y-x" f] by auto

lemma propev_to_propseq:
  fixes tr ee i j p k es'
  assumes a0: "valid_gtrace tr"
  and c3:"exseq tr p j = Some esj" "es_active esj"
  and c4:"i \<le> j"
  and a2:"\<forall> e . ge_n e \<in> {i..j} \<and> globev tr e \<and> ge_proc e = p \<longrightarrow> A (ev_stm e)"
  and h1:"k \<in> {i..j}" "exseq tr p k = Some es'"
  shows "A (es_stm es')"
proof -
  have h2:"etrans (exseq tr p k) (exseq tr p (Suc k))" using a0(1) exseq_trans by simp
  from this h1 obtain es'' where h3:"exseq tr p (Suc k) = Some es''" using etrans_cont by blast

  obtain lset where d1:"lset = { l . l \<in> {k..j} \<and> (\<exists> es' . exseq tr p l = Some es' \<and> es_active es' ) }" by blast
  from c3 c4 d1 h1 have "j \<in> lset" by auto
  then obtain k' where d2:"k' \<in> lset \<and> (\<forall> l. l \<in> lset \<longrightarrow> k' \<preceq> l)" using Hilbert_Choice.ex_has_least_nat mem_def by metis
  from this d1 obtain es1 where d3:"exseq tr p k' = Some es1" by blast
  from d2 d1 this have d4:"k' \<in> {k..j} \<and> es_active es1" by simp
  have "etrans (exseq tr p k') (exseq tr p (Suc k'))" using a0(1) exseq_trans by simp
  from this d3 obtain es2 where d5:"exseq tr p (Suc k') = Some es2" using etrans_cont by blast

  have h4:"k < k' \<longrightarrow> es_stm es'' = es_stm es'"
  proof
    assume "k < k'"
    from this d2 have "k \<notin> lset" by auto
    from this h1 d1 have "\<not> es_active es'" by auto
    from this h1 h2 h3 show "es_stm es'' = es_stm es'" by (cases es', cases es'', auto)
  qed
    (*--------------------------------*)
  have eseq1:"es_stm es1 = es_stm es'"
  proof -
    have z1:"\<forall> l . l \<ge> Suc k \<and> l \<le> (k'-(1::nat)) \<longrightarrow> es_stm (the (exseq tr p l)) = es_stm (the (exseq tr p (Suc l)))"
    proof clarify
      fix l
      assume f1:"l \<ge> Suc k" "l \<le> (k'-(1::nat))"
      then have "l \<le> k'" by auto
      from a0(1) d3 this have "exseq tr p l \<noteq> None" using exseq_pre by (metis option.simps(2))
      then obtain esx where f2:"exseq tr p l = Some esx" by auto
      have f3:"\<not> es_active esx"
      proof -
        from f1 d4 have "l \<in> {k..j}" by auto
        from this f2 d1 have "es_active esx \<longrightarrow> l \<in> lset" by auto
        moreover from f1 d2 have "l \<in> lset \<longrightarrow> False" by auto
        ultimately show ?thesis by blast
      qed
      from a0 have f4:"etrans (exseq tr p l) (exseq tr p (Suc l))" using exseq_trans by simp
      from this f2 obtain esy where f5:"exseq tr p (Suc l) = Some esy" using etrans_cont by blast
      from f2 f3 f4 f5 show "es_stm (the (exseq tr p l)) = es_stm (the (exseq tr p (Suc l)))"
        apply(cases "exseq tr p l", auto)
        by (cases esx, auto)
    qed
    from h1 d4 have "k \<le> k'" by auto
    then have "(k'\<ge>1 \<and> Suc k \<le> (k' - (1::nat))) \<or> (k' = Suc k) \<or> (k' = k)" by auto
    moreover {
      assume u1:"k'\<ge>1 \<and> Suc k \<le> (k' - (1::nat))"
      moreover from this z1 have "(es_stm (the (exseq tr p (Suc k)))) = (es_stm (the (exseq tr p k')))" using lem_ntran_helper2 [of "Suc k" "k'-(1::nat)" "\<lambda> x .es_stm (the (exseq tr p x))"] by auto
      ultimately have "es_stm es1 = es_stm es''" using h3 d3 by auto
      moreover from u1 have "k < k'" by auto
      ultimately have ?thesis using h4 by simp
    }
    moreover {
      assume u1:"k' = Suc k"
      then have "k < k'" by auto
      moreover from h3 d3 u1 have "es_stm es1 = es_stm es''" by simp
      ultimately have ?thesis using h4 by simp
    }
    moreover {
      assume "k' = k"
      from this d3 h1 have ?thesis by simp
    }
    ultimately show ?thesis by blast
  qed
    (*--------------------------------*)
  from d3 d4 d5 obtain stp where r1:"estepev (the (exseq tr p k')) (the (exseq tr p (Suc k'))) stp"
    by (cases es1, cases es2, auto)
  obtain e where r2:"e = (Gevent k' p stp)" by blast
  from d5 r1 r2 a0(1) have r3:"globev tr e" using exseq_to_ev by (metis option.simps(3))
  from d4 h1 r2 have "ge_n e \<in> {i..j}" by (subgoal_tac "ge_n e = k'", auto)
  from this r2 r3 have "A (ev_stm e)" using a2 by (metis ge_proc.simps)
  moreover have "es_of_ev e = es1"
  proof -
    from r2 have "ge_n e = k' \<and> ge_proc e = p" by auto
    from a0(1) this r3 have "exseq tr p k' = Some (es_of_ev e)" using esevent by auto
    from this d3 show ?thesis by simp
  qed
  ultimately show "A (es_stm es')" using eseq1 by auto
qed

lemma lem_ev_astmcl:
  fixes A tr e1 e2 p
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr" "globev tr e1" "globev tr e2"
  and a1: "e1 \<preceq> e2" "ge_proc e1 = p" "ge_proc e2 = p"
  and a2: "\<forall> e \<in> {e1<..e2} . globev tr e \<and> ge_proc e = p \<longrightarrow> A (ev_stm e)" "A (ev_stm e2)"
  shows "astmcl A (ev_stm e1) (ev_stm e2)"
proof -
  obtain i j where c1: "i = ge_n e1 \<and> j = ge_n e2" by blast
  from a0 a1 c1 have c2:"exseq tr p i = Some (es_of_ev e1)" using ev_in_exseq by metis
  moreover from a0 a1 c1 have c3:"exseq tr p j = Some (es_of_ev e2)" using ev_in_exseq by metis
  moreover from a1(1) c1 have c4:"i \<le> j" using less_eq_gevent_def by blast
  moreover have "\<forall>k\<in>{i<..j}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')"
  proof clarify
    fix k es'
    assume h1:"k \<in> {i<..j}" "exseq tr p k = Some es'"
    from h1 have h2: "k \<in> {Suc i..j}" "Suc i \<le> j" "es_active (es_of_ev e2)" by auto
    have "\<forall> e . ge_n e \<in> {Suc i..j} \<and> globev tr e \<and> ge_proc e = p \<longrightarrow> A (ev_stm e)"
    proof
      fix e
      { assume zz1:"ge_n e \<in> {Suc i..j}" "globev tr e" "ge_proc e = p"
      then have "ge_n e \<in> {i<..j}" by auto
      from this c1 have "e \<in> {e1<..e2}" using less_eq_gevent_def less_gevent_def by auto
      from this zz1 a2 have "A (ev_stm e)" by blast
      }
      then show "ge_n e \<in> {Suc i..j} \<and> globev tr e \<and> ge_proc e = p \<longrightarrow> A (ev_stm e)" by blast
    qed
    from a0(1) h1 h2 c3 this show "A (es_stm es')" using propev_to_propseq [of tr p j "(es_of_ev e2)" "Suc i" A k es'] by metis
  qed
  moreover from a2 have "A (es_stm (es_of_ev e2))" by simp
  ultimately have "astmcl A (es_stm (es_of_ev e1)) (es_stm (es_of_ev e2))" using a0 lem_exseq_astmcl acond by metis
  then show ?thesis by simp
qed

(*
lemma lem_ev_astmcl:
  fixes A tr e1 e2 p
  assumes acond: "seqcond A"
  and a0: "valid_gtrace tr" "globev tr e1" "globev tr e2"
  and a1: "e1 \<preceq> e2" "ge_proc e1 = p" "ge_proc e2 = p"
  and a2: "\<forall> e \<in> {e1<..e2} . globev tr e \<and> ge_proc e = p \<longrightarrow> A (ev_stm e)" "A (ev_stm e2)"
  shows "astmcl A (ev_stm e1) (ev_stm e2)"
proof -
  obtain i j where c1: "i = ge_n e1 \<and> j = ge_n e2" by blast
  from a0 a1 c1 have c2:"exseq tr p i = Some (es_of_ev e1)" using ev_in_exseq by metis
  moreover from a0 a1 c1 have c3:"exseq tr p j = Some (es_of_ev e2)" using ev_in_exseq by metis
  moreover from a1(1) c1 have c4:"i \<le> j" using less_eq_gevent_def by blast
  moreover have "\<forall>k\<in>{i<..j}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')"
  proof clarify
    fix k es'
    assume h1:"k \<in> {i<..j}" "exseq tr p k = Some es'"
    have h2:"etrans (exseq tr p k) (exseq tr p (Suc k))" using a0(1) exseq_trans by simp
    from this h1 obtain es'' where h3:"exseq tr p (Suc k) = Some es''" using etrans_cont by blast

    obtain lset where d1:"lset = { l . l \<in> {k..j} \<and> (\<exists> es' . exseq tr p l = Some es' \<and> es_active es' ) }" by blast
    from c3 c4 d1 h1 have "j \<in> lset" by auto
    then obtain k' where d2:"k' \<in> lset \<and> (\<forall> l. l \<in> lset \<longrightarrow> k' \<preceq> l)" using Hilbert_Choice.ex_has_least_nat mem_def by metis
    from this d1 obtain es1 where d3:"exseq tr p k' = Some es1" by blast
    from d2 d1 this have d4:"k' \<in> {k..j} \<and> es_active es1" by simp
    have "etrans (exseq tr p k') (exseq tr p (Suc k'))" using a0(1) exseq_trans by simp
    from this d3 obtain es2 where d5:"exseq tr p (Suc k') = Some es2" using etrans_cont by blast

    have h4:"k < k' \<longrightarrow> es_stm es'' = es_stm es'"
    proof
      assume "k < k'"
      from this d2 have "k \<notin> lset" by auto
      from this h1 d1 have "\<not> es_active es'" by auto
      from this h1 h2 h3 show "es_stm es'' = es_stm es'" by (cases es', cases es'', auto)
    qed
    (*--------------------------------*)
    have eseq1:"es_stm es1 = es_stm es'"
    proof -
      have z1:"\<forall> l . l \<ge> Suc k \<and> l \<le> (k'-(1::nat)) \<longrightarrow> es_stm (the (exseq tr p l)) = es_stm (the (exseq tr p (Suc l)))"
      proof clarify
        fix l
        assume f1:"l \<ge> Suc k" "l \<le> (k'-(1::nat))"
        then have "l \<le> k'" by auto
        from a0(1) d3 this have "exseq tr p l \<noteq> None" using exseq_pre by (metis option.simps(2))
        then obtain esx where f2:"exseq tr p l = Some esx" by auto
        have f3:"\<not> es_active esx"
        proof -
          from f1 d4 have "l \<in> {k..j}" by auto
          from this f2 d1 have "es_active esx \<longrightarrow> l \<in> lset" by auto
          moreover from f1 d2 have "l \<in> lset \<longrightarrow> False" by auto
          ultimately show ?thesis by blast
        qed
        from a0 have f4:"etrans (exseq tr p l) (exseq tr p (Suc l))" using exseq_trans by simp
        from this f2 obtain esy where f5:"exseq tr p (Suc l) = Some esy" using etrans_cont by blast
        from f2 f3 f4 f5 show "es_stm (the (exseq tr p l)) = es_stm (the (exseq tr p (Suc l)))"
          apply(cases "exseq tr p l", auto)
          by (cases esx, auto)
      qed
      from h1 d4 have "k \<le> k'" by auto
      then have "(k'\<ge>1 \<and> Suc k \<le> (k' - (1::nat))) \<or> (k' = Suc k) \<or> (k' = k)" by auto
      moreover {
        assume u1:"k'\<ge>1 \<and> Suc k \<le> (k' - (1::nat))"
        moreover from this z1 have "(es_stm (the (exseq tr p (Suc k)))) = (es_stm (the (exseq tr p k')))" using lem_ntran_helper2 [of "Suc k" "k'-(1::nat)" "\<lambda> x .es_stm (the (exseq tr p x))"] by auto
        ultimately have "es_stm es1 = es_stm es''" using h3 d3 by auto
        moreover from u1 have "k < k'" by auto
        ultimately have ?thesis using h4 by simp
      }
      moreover {
        assume u1:"k' = Suc k"
        then have "k < k'" by auto
        moreover from h3 d3 u1 have "es_stm es1 = es_stm es''" by simp
        ultimately have ?thesis using h4 by simp
      }
      moreover {
        assume "k' = k"
        from this d3 h1 have ?thesis by simp
      }
      ultimately show ?thesis by blast
    qed
    (*--------------------------------*)
    from d3 d4 d5 obtain stp where r1:"estepev (the (exseq tr p k')) (the (exseq tr p (Suc k'))) stp"
      by (cases es1, cases es2, auto)
    obtain e where r2:"e = (Gevent k' p stp)" by blast
    from d5 r1 r2 a0(1) have r3:"globev tr e" using exseq_to_ev by (metis option.simps(3))
    have "e \<in> {e1<..e2}"
    proof -
      from d4 h1 c1 r2 have "ge_n e1 < ge_n e \<and> ge_n e \<le> ge_n e2" by simp
      then show ?thesis using less_gevent_def less_eq_gevent_def by auto
    qed
    from this r2 r3 have "A (ev_stm e)" using a2 by (metis ge_proc.simps)
    moreover have "es_of_ev e = es1"
    proof -
      from r2 have "ge_n e = k' \<and> ge_proc e = p" by auto
      from a0(1) this r3 have "exseq tr p k' = Some (es_of_ev e)" using esevent by auto
      from this d3 show ?thesis by simp
    qed
    ultimately show "A (es_stm es')" using eseq1 by auto
  qed
  moreover from a2 have "A (es_stm (es_of_ev e2))" by simp
  ultimately have "astmcl A (es_stm (es_of_ev e1)) (es_stm (es_of_ev e2))" using a0 lem_exseq_astmcl acond by metis
  then show ?thesis by simp
qed
*)

lemma lem_init_astmcl:
  assumes acond: "seqcond A"
  and a0: "prog_semantics pg tr"
  and a1:"globev tr e" "proc \<in> set pg" "p = proc_name proc" "p = ge_proc e"
  and a2: "\<forall> e' \<le> e . globev tr e' \<and> ge_proc e' = p \<longrightarrow> A (ev_stm e')"
  shows "astmcl A (proc_stm proc) (ev_stm e)"
proof -
  from a0 a1 obtain io bv where c0:"exseq tr (ge_proc e) 0 = Some (Estate (proc_stm proc) empty io bv)" using exseq_init by blast
  obtain i where c2:"ge_n e = i" by blast
  from a0 have c3:"valid_gtrace tr" using prog_semantics_def by blast

  obtain es where d0:"es = (Estate (proc_stm proc) empty io bv)" by blast
  from c3 c2 a1(3) a1(4) a1(1) have d1:"exseq tr p i = Some (es_of_ev e)" using ev_in_exseq by metis
  from d0 c0 a1 have d2:"exseq tr p 0 = Some es" by simp
  have d3:"0 \<le> i" by auto
  moreover have "\<forall>k \<in> {0..i}. \<forall>es'. exseq tr p k = Some es' \<longrightarrow> A (es_stm es')"
  proof clarify
    fix k es'
    assume h1:"k \<in> {0..i}" "exseq tr p k = Some es'"
    have h2: "es_active (es_of_ev e)" by auto
    have "\<forall> e' . ge_n e' \<in> {0..i} \<and> globev tr e' \<and> ge_proc e' = p \<longrightarrow> A (ev_stm e')"
    proof
      fix e'
      { assume zz1:"ge_n e' \<in> {0..i}" "globev tr e'" "ge_proc e' = p"
      then have "ge_n e' \<in> {0..i}" by auto
      from this c2 have "e' \<preceq> e" using less_eq_gevent_def less_gevent_def by auto
      from this zz1 a2 have "A (ev_stm e')" by blast
      }
      then show "ge_n e' \<in> {0..i} \<and> globev tr e' \<and> ge_proc e' = p \<longrightarrow> A (ev_stm e')" by blast
    qed
    from c3 d1 d3 h1 h2 this show "A (es_stm es')" using propev_to_propseq [of tr p i "(es_of_ev e)" "0" A k es'] by metis
  qed
  ultimately have "astmcl A (es_stm es) (es_stm (es_of_ev e))" using d1 d2 c3 lem_exseq_astmcl_closed acond by metis
  from d0 this show ?thesis by simp
qed

end
